| Definitions | t  T, s = t, ES, AbsInterface(A), {x:A| B(x)} , f(a), Type, x:A  B(x),  x:A. B(x), E, x:A  B(x),  b, left + right, let x,y = A in B(x;y), t.1, chain_config(), decidable is-tail, X(e), cctail?(x), e  X, P & Q,  e<e'.P(e), Dec(P),  , loc(e), Id,  , E(X), a:A fp B(a), strong-subtype(A;B), P   Q, <a, b>, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi ,  , Unit, ff, inr x , "$token", inl x , tt, Atom, Top, False, True, A c B, EqDecider(T), IdLnk, EOrderAxioms(E; pred?; info), EState(T), Knd,   x. t(x), x,y. t(x;y), kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), type List,  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r  s, constant_function(f;A;B), loc(e), kind(e), x.A(x), (e <loc e'),  A, SWellFounded(R(x;y)), pred!(e;e'), Void,  x:A.B(x), S  T, suptype(S; T), first(e), pred(e), tail-dcdr{i:l}(es;Config) |